Theorem 3impia 1115

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  mopick2  2639  3gencl  3463  vtoclgft  3482  mob2  3645  moi  3648  reupick3  4250  disjne  4385  elpr2elpr  4796  disji2  5052  disji  5053  tz7.2  5564  sofld  6079  ordintdif  6300  funopg  6452  fvun1  6841  fvopab6  6890  fveqressseq  6939  fvcofneq  6951  fprg  7009  2f1fvneq  7114  isores3  7186  ovmpt4g  7398  ovmpos  7399  ov2gf  7400  ofrval  7523  sorpssuni  7563  sorpssint  7564  poxp  7940  suppss2  7987  frrlem12  8084  smoel  8162  smoord  8167  smogt  8169  oaass  8354  oewordi  8384  oeoalem  8389  oeoelem  8391  nnawordi  8414  nnaass  8415  qsel  8543  xpdom3  8810  onsdominel  8862  mapdom3  8885  fisseneq  8963  cantnflem1  9377  cfslbn  9954  cfsmolem  9957  cfcoflem  9959  infpssrlem4  9993  fin23lem7  10003  fin23lem25  10011  isf34lem7  10066  hsmexlem2  10114  axcc3  10125  axdc4lem  10142  tskss  10445  gruss  10483  gruurn  10485  gruiun  10486  gruel  10490  gruen  10499  grudomon  10504  grothac  10517  axpre-sup  10856  axsup  10981  addn0nid  11325  letrp1  11749  p1le  11750  lemul1a  11759  infrelb  11890  zextle  12323  zextlt  12324  btwnnz  12326  gtndiv  12327  uzind2  12343  fzind  12348  eluzsub  12543  zsupss  12606  xrltne  12826  lemaxle  12858  qbtwnre  12862  qbtwnxr  12863  xlemul1a  12951  icogelb  13059  iccleub  13063  iccsplit  13146  uzsubsubfz  13207  elfz0fzfz0  13290  difelfznle  13299  fvffz0  13303  elfzo0le  13359  fzonmapblen  13361  fzofzim  13362  ceile  13497  modadd1  13556  muladdmodid  13559  modmul1  13572  modirr  13590  fsuppmapnn0fiub0  13641  expcl2lem  13722  expclzlem  13734  expnegz  13745  leexp2r  13820  bcval4  13949  bccmpl  13951  hashbnd  13978  hashunsnggt  14037  hashgt23el  14067  elovmpowrd  14189  ccatval2  14211  ccatrcl1  14227  wrdl1s1  14247  ccat2s1fvw  14277  ccat2s1fvwOLD  14278  swrdsb0eq  14304  swrdccatin1  14366  pfxccatpfx2  14378  repswswrd  14425  cshwcsh2id  14469  absexpz  14945  climbdd  15311  iseraltlem2  15322  binomfallfac  15679  dvdsle  15947  divalgb  16041  ndvdssub  16046  dvdsgcd  16180  dfgcd2  16182  rplpwr  16195  lcmgcdlem  16239  lcmfunsn  16277  coprmdvds1  16285  qredeq  16290  2mulprm  16326  prmdvdsexpr  16350  nnnn0modprm0  16435  prm23ge5  16444  pcexp  16488  difsqpwdvds  16516  prmpwdvds  16533  ramcl  16658  cshwshashlem3  16727  cshwrepswhash1  16732  elrestr  17056  mreintcl  17221  mremre  17230  mrieqv2d  17265  initoeu2lem1  17645  funcestrcsetclem9  17781  funcsetcestrclem9  17796  prstr  17933  drsdirfi  17938  latnlej  18089  latnlej2  18092  acsdrsel  18176  acsdrscl  18179  mrelatglb  18193  mrelatlub  18195  isnmgm  18245  grpasscan1  18553  grpinvnz  18561  mulgneg2  18652  gsmsymgrfix  18951  f1omvdco2  18971  symggen  18993  odcl2  19087  odhash3  19096  lsmss1  19186  lsmss2  19188  efgred  19269  efgcpbl  19277  ablfacrp  19584  ablfac1eu  19591  ablfaclem3  19605  dvdsrmul1  19810  dvdsunit  19820  irredmul  19866  lmodlema  20043  psgnodpmr  20707  phlssphl  20776  lindsss  20941  lindfmm  20944  ply1scln0  21372  dmatelnd  21553  mdetdiaglem  21655  mdet0  21663  mdetunilem7  21675  slesolinv  21737  cramerimplem3  21742  cpmatpmat  21767  m2cpminvid2lem  21811  chfacfscmul0  21915  chfacfpmmul0  21919  riinopn  21965  clsndisj  22134  cnpf2  22309  hausnei2  22412  cmpcov  22448  cmpfii  22468  unconn  22488  t1connperf  22495  nrmr0reg  22808  fbfinnfr  22900  filuni  22944  alexsubALT  23110  tmdgsum  23154  cuspcvg  23361  mopni  23554  isngp4  23674  metdsre  23922  iimulcl  24006  phtpc01  24065  clmmulg  24170  cfilucfil4  24390  bcthlem5  24397  bcth  24398  bcth3  24400  itg1le  24783  itg2le  24809  bddmulibl  24908  bddiblnc  24911  dvnres  25000  cpnord  25004  dvnfre  25021  deg1ge  25168  dgr1term  25326  aaliou3lem2  25408  sincosq1lem  25559  cxpge0  25743  cxpmul2  25749  logrec  25818  logbgcd1irr  25849  sqfpc  26191  bcmono  26330  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem4  26422  2lgsoddprmlem3  26467  pntrmax  26617  qabvexp  26679  ostth2lem2  26687  ax5seglem4  27203  axeuclidlem  27233  uhgredgrnv  27403  usgredg4  27487  nbuhgr2vtx1edgblem  27621  vtxduhgr0e  27748  vtxduhgr0nedg  27762  rusgrpropnb  27853  uspgr2wlkeqi  27917  redwlklem  27941  lfgrwlkprop  27957  2pthnloop  28000  spthonepeq  28021  pthdlem2lem  28036  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  crctcshwlkn0lem7  28082  crctcshwlkn0  28087  wlkiswwlks1  28133  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wwlksnext  28159  wwlksnextproplem2  28176  wspthsnonn0vne  28183  2pthon3v  28209  rusgrnumwwlk  28241  erclwwlkeqlen  28284  erclwwlksym  28286  erclwwlktr  28287  erclwwlkneqlen  28333  erclwwlknsym  28335  erclwwlkntr  28336  uhgr3cyclex  28447  upgreupthseg  28474  eupth2lem3lem4  28496  eucrctshift  28508  4cycl2vnunb  28555  nvs  28926  nvtri  28933  nmlno0  29058  nmlnoubi  29059  ubth  29136  hlipgt0  29177  ocnel  29561  elspansn2  29830  elspansn3  29835  normcan  29839  pjoml2  29874  lecm  29880  osum  29908  nmbdfnlb  30313  leopmul  30397  hstpyth  30492  cvnbtwn  30549  ssmd1  30574  ssmd2  30575  ssdmd1  30576  ssdmd2  30577  cvmd  30599  cvdmd  30600  superpos  30617  disji2f  30817  disjif  30818  disjif2  30821  preiman0  30944  padct  30956  ffs2  30965  bcm1n  31018  s2f1  31121  omndadd  31234  ogrpaddlt  31245  archiabl  31354  slmdlema  31358  lbslsat  31601  eulerpartlemb  32235  sgn3da  32408  fisshasheq  32973  hashfundm  32974  cvmsdisj  33132  cvmlift2lem12  33176  satfrel  33229  satfrnmapom  33232  fmlasuc  33248  satffun  33271  satef  33278  sategoelfv  33282  ttrclss  33706  poseq  33729  naddssim  33764  nosepon  33795  nolesgn2o  33801  nogesgn1o  33803  nosepnelem  33809  nosepne  33810  nosepdmlem  33813  nosepdm  33814  nodenselem8  33821  noresle  33827  noetasuplem4  33866  noetainflem4  33870  scutbdaylt  33939  lineintmo  34386  nn0prpwlem  34438  nn0prpw  34439  neibastop2lem  34476  lindsadd  35697  areacirc  35797  incsequz  35833  mettrifi  35842  ismtybnd  35892  heiborlem1  35896  rngoisocnv  36066  risci  36072  eqvrelqsel  36656  lfl1  37011  lkrlsp2  37044  omlfh3N  37200  cvrnbtwn  37212  cvrnbtwn2  37216  cvrnbtwn4  37220  cvlexch3  37273  cvlexch4N  37274  cvlatexchb1  37275  2llnne2N  37349  atcvrj0  37369  cvrat2  37370  ps-1  37418  3atlem5  37428  islln2a  37458  lplnriaN  37491  lplnribN  37492  llncvrlpln2  37498  lplncvrlvol2  37556  psubatN  37696  pmapglb2N  37712  pmapglb2xN  37713  2llnma1b  37727  paddasslem17  37777  pmod2iN  37790  pmodl42N  37792  hlmod1i  37797  atmod1i1  37798  atmod1i2  37800  llnmod1i2  37801  pclcmpatN  37842  osumcllem8N  37904  pexmidlem3N  37913  pl42lem4N  37923  4atexlem7  38016  ltrnnid  38077  cdlemc4  38135  cdleme32a  38382  cdlemeg46gfre  38473  cdlemf2  38503  cdlemg4c  38553  trlcoat  38664  tendovalco  38706  tendoeq2  38715  cdlemk36  38854  diael  38984  diatrl  38985  dicelval1stN  39129  dicelval2nd  39130  dihlspsnat  39274  dochkr1  39419  lcfrlem9  39491  mapdh8e  39725  hdmapval0  39774  hgmapval0  39833  nnadddir  40221  nn0rppwr  40254  nn0expgcd  40256  dvdsexpnn0  40262  incssnn0  40449  pell14qrexpcl  40605  pell14qrgap  40613  congadd  40704  acongsym  40714  acongtr  40716  dvdsacongtr  40722  jm2.19lem3  40729  jm2.19lem4  40730  jm2.26lem3  40739  ismnushort  41808  bi13impia  41997  3impcombi  42326  ioogtlb  42923  iocgtlb  42930  iocleub  42931  icoltub  42936  iooltub  42938  limclner  43082  limsupre3lem  43163  climuzlem  43174  elfzelfzlble  44701  subsubelfzo0  44706  iccpartigtl  44763  sqrtpwpw2p  44878  fmtnoprmfac1lem  44904  fmtno4prmfac  44912  evenltle  45057  even3prm2  45059  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem1  45145  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  upgrwlkupwlk  45190  c0snmgmhm  45360  funcringcsetcALTV2lem9  45490  funcringcsetclem9ALTV  45513  lincscmcl  45661  lindslinindimp2lem4  45690  lincresunit2  45707  lincresunit3  45710  elfzolborelfzop1  45748  m1modmmod  45755  rege1logbzge0  45793  fllog2  45802  dignn0ldlem  45836  rrx2pnecoorneor  45949  rrx2plord2  45956  rrx2linest  45976  ipolub  46162  ipoglb  46165