Theorem 3impia 1117

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 1116	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mopick2  2640  ceqsalt  3523  3gencl  3535  vtoclgft  3564  vtoclegft  3601  rspc6v  3656  mob2  3737  moi  3740  reupick3  4349  disjne  4478  elpr2elpr  4893  disji2  5150  disji  5151  tz7.2  5683  sofld  6218  ordintdif  6445  funopg  6612  fvun1  7013  fvopab6  7063  fveqressseq  7113  fvcofneq  7127  fprg  7189  2f1fvneq  7297  isores3  7371  ovmpt4g  7597  ovmpos  7598  ov2gf  7599  ofrval  7726  sorpssuni  7767  sorpssint  7768  poxp  8169  poseq  8199  suppss2  8241  frrlem12  8338  smoel  8416  smoord  8421  smogt  8423  oaass  8617  oewordi  8647  oeoalem  8652  oeoelem  8654  nnawordi  8677  nnaass  8678  naddssim  8741  qsel  8854  xpdom3  9136  onsdominel  9192  mapdom3  9215  sdomdomtrfi  9267  domsdomtrfi  9268  php  9273  onomeneq  9291  fisseneq  9320  fodomfir  9396  cantnflem1  9758  ttrclss  9789  cfslbn  10336  cfsmolem  10339  cfcoflem  10341  infpssrlem4  10375  fin23lem7  10385  fin23lem25  10393  isf34lem7  10448  hsmexlem2  10496  axcc3  10507  axdc4lem  10524  tskss  10827  gruss  10865  gruurn  10867  gruiun  10868  gruel  10872  gruen  10881  grudomon  10886  grothac  10899  axpre-sup  11238  axsup  11365  addn0nid  11710  letrp1  12138  p1le  12139  lemul1a  12148  infrelb  12280  zextle  12716  zextlt  12717  btwnnz  12719  gtndiv  12720  uzind2  12736  fzind  12741  eluzsubOLD  12939  zsupss  13002  xrltne  13225  lemaxle  13257  qbtwnre  13261  qbtwnxr  13262  xlemul1a  13350  icogelb  13458  iccleub  13462  iccsplit  13545  uzsubsubfz  13606  elfz0fzfz0  13690  difelfznle  13699  fvffz0  13703  elfzo0le  13760  fzonmapblen  13762  fzofzim  13763  ceile  13900  modadd1  13959  muladdmodid  13962  modmul1  13975  modirr  13993  fsuppmapnn0fiub0  14044  expcl2lem  14124  expclzlem  14134  expnegz  14147  leexp2r  14224  bcval4  14356  bccmpl  14358  hashbnd  14385  hashunsnggt  14443  hashgt23el  14473  hashfundm  14491  elovmpowrd  14606  ccatval2  14626  ccatrcl1  14642  wrdl1s1  14662  ccat2s1fvw  14686  swrdsb0eq  14711  swrdccatin1  14773  pfxccatpfx2  14785  repswswrd  14832  cshwcsh2id  14877  absexpz  15354  climbdd  15720  iseraltlem2  15731  binomfallfac  16089  dvdsle  16358  divalgb  16452  ndvdssub  16457  dvdsgcd  16591  dfgcd2  16593  rplpwr  16605  nn0rppwr  16608  nn0expgcd  16611  lcmgcdlem  16653  lcmfunsn  16691  coprmdvds1  16699  qredeq  16704  2mulprm  16740  prmdvdsexpr  16764  nnnn0modprm0  16853  prm23ge5  16862  pcexp  16906  difsqpwdvds  16934  prmpwdvds  16951  ramcl  17076  cshwshashlem3  17145  cshwrepswhash1  17150  elrestr  17488  mreintcl  17653  mremre  17662  mrieqv2d  17697  initoeu2lem1  18081  funcestrcsetclem9  18217  funcsetcestrclem9  18232  prstr  18370  drsdirfi  18375  latnlej  18526  latnlej2  18529  acsdrsel  18613  acsdrscl  18616  mrelatglb  18630  mrelatlub  18632  isnmgm  18682  grpasscan1  19041  grpinvnz  19050  mulgneg2  19148  gsmsymgrfix  19470  f1omvdco2  19490  symggen  19512  odcl2  19607  odhash3  19618  lsmss1  19707  lsmss2  19709  efgred  19790  efgcpbl  19798  ablfacrp  20110  ablfac1eu  20117  ablfaclem3  20131  dvdsrmul1  20395  dvdsunit  20405  irredmul  20455  c0snmgmhm  20488  lmodlema  20885  psgnodpmr  21631  phlssphl  21700  lindsss  21867  lindfmm  21870  ply1scln0  22316  dmatelnd  22523  mdetdiaglem  22625  mdet0  22633  mdetunilem7  22645  slesolinv  22707  cramerimplem3  22712  cpmatpmat  22737  m2cpminvid2lem  22781  chfacfscmul0  22885  chfacfpmmul0  22889  riinopn  22935  clsndisj  23104  cnpf2  23279  hausnei2  23382  cmpcov  23418  cmpfii  23438  unconn  23458  t1connperf  23465  nrmr0reg  23778  fbfinnfr  23870  filuni  23914  alexsubALT  24080  tmdgsum  24124  cuspcvg  24331  mopni  24526  isngp4  24646  metdsre  24894  iimulcl  24985  phtpc01  25047  clmmulg  25153  cfilucfil4  25374  bcthlem5  25381  bcth  25382  bcth3  25384  itg1le  25768  itg2le  25794  bddmulibl  25894  bddiblnc  25897  dvnres  25987  cpnord  25991  dvnfre  26010  deg1ge  26157  dgr1term  26319  aaliou3lem2  26403  sincosq1lem  26557  cxpge0  26743  cxpmul2  26749  logrec  26824  logbgcd1irr  26855  sqfpc  27198  bcmono  27339  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  gausslemma2dlem4  27431  2lgsoddprmlem3  27476  pntrmax  27626  qabvexp  27688  ostth2lem2  27696  nosepon  27728  nolesgn2o  27734  nogesgn1o  27736  nosepnelem  27742  nosepne  27743  nosepdmlem  27746  nosepdm  27747  nodenselem8  27754  noresle  27760  noetasuplem4  27799  noetainflem4  27803  scutbdaylt  27881  addsuniflem  28052  ssltmul1  28191  precsexlem6  28254  precsexlem7  28255  precsexlem11  28259  sltonold  28301  ax5seglem4  28965  axeuclidlem  28995  uhgredgrnv  29165  usgredg4  29252  nbuhgr2vtx1edgblem  29386  vtxduhgr0e  29514  vtxduhgr0nedg  29528  rusgrpropnb  29619  uspgr2wlkeqi  29684  redwlklem  29707  lfgrwlkprop  29723  2pthnloop  29767  spthonepeq  29788  pthdlem2lem  29803  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  crctcshwlkn0lem7  29849  crctcshwlkn0  29854  wlkiswwlks1  29900  wlkiswwlks2  29908  wlkiswwlksupgr2  29910  wwlksnext  29926  wwlksnextproplem2  29943  wspthsnonn0vne  29950  2pthon3v  29976  rusgrnumwwlk  30008  erclwwlkeqlen  30051  erclwwlksym  30053  erclwwlktr  30054  erclwwlkneqlen  30100  erclwwlknsym  30102  erclwwlkntr  30103  uhgr3cyclex  30214  upgreupthseg  30241  eupth2lem3lem4  30263  eucrctshift  30275  4cycl2vnunb  30322  nvs  30695  nvtri  30702  nmlno0  30827  nmlnoubi  30828  ubth  30905  hlipgt0  30946  ocnel  31330  elspansn2  31599  elspansn3  31604  normcan  31608  pjoml2  31643  lecm  31649  osum  31677  nmbdfnlb  32082  leopmul  32166  hstpyth  32261  cvnbtwn  32318  ssmd1  32343  ssmd2  32344  ssdmd1  32345  ssdmd2  32346  cvmd  32368  cvdmd  32369  superpos  32386  disji2f  32599  disjif  32600  disjif2  32603  preiman0  32721  padct  32733  ffs2  32742  bcm1n  32800  s2f1  32911  omndadd  33056  ogrpaddlt  33067  archiabl  33178  slmdlema  33182  lbslsat  33629  eulerpartlemb  34333  sgn3da  34506  fisshasheq  35082  cvmsdisj  35238  cvmlift2lem12  35282  satfrel  35335  satfrnmapom  35338  fmlasuc  35354  satffun  35377  satef  35384  sategoelfv  35388  lineintmo  36121  nn0prpwlem  36288  nn0prpw  36289  neibastop2lem  36326  lindsadd  37573  areacirc  37673  incsequz  37708  mettrifi  37717  ismtybnd  37767  heiborlem1  37771  rngoisocnv  37941  risci  37947  eqvrelqsel  38572  lfl1  39026  lkrlsp2  39059  omlfh3N  39215  cvrnbtwn  39227  cvrnbtwn2  39231  cvrnbtwn4  39235  cvlexch3  39288  cvlexch4N  39289  cvlatexchb1  39290  2llnne2N  39365  atcvrj0  39385  cvrat2  39386  ps-1  39434  3atlem5  39444  islln2a  39474  lplnriaN  39507  lplnribN  39508  llncvrlpln2  39514  lplncvrlvol2  39572  psubatN  39712  pmapglb2N  39728  pmapglb2xN  39729  2llnma1b  39743  paddasslem17  39793  pmod2iN  39806  pmodl42N  39808  hlmod1i  39813  atmod1i1  39814  atmod1i2  39816  llnmod1i2  39817  pclcmpatN  39858  osumcllem8N  39920  pexmidlem3N  39929  pl42lem4N  39939  4atexlem7  40032  ltrnnid  40093  cdlemc4  40151  cdleme32a  40398  cdlemeg46gfre  40489  cdlemf2  40519  cdlemg4c  40569  trlcoat  40680  tendovalco  40722  tendoeq2  40731  cdlemk36  40870  diael  41000  diatrl  41001  dicelval1stN  41145  dicelval2nd  41146  dihlspsnat  41290  dochkr1  41435  lcfrlem9  41507  mapdh8e  41741  hdmapval0  41790  hgmapval0  41849  nnadddir  42259  dvdsexpnn0  42321  incssnn0  42667  pell14qrexpcl  42823  pell14qrgap  42831  congadd  42923  acongsym  42933  acongtr  42935  dvdsacongtr  42941  jm2.19lem3  42948  jm2.19lem4  42949  jm2.26lem3  42958  onexlimgt  43204  nadd2rabex  43348  ismnushort  44270  bi13impia  44459  3impcombi  44788  ioogtlb  45413  iocgtlb  45420  iocleub  45421  icoltub  45426  iooltub  45428  limclner  45572  limsupre3lem  45653  climuzlem  45664  fsupdm  46763  finfdm  46767  elfzelfzlble  47236  subsubelfzo0  47241  iccpartigtl  47297  sqrtpwpw2p  47412  fmtnoprmfac1lem  47438  fmtno4prmfac  47446  evenltle  47591  even3prm2  47593  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  bgoldbtbndlem1  47679  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  uhgrimisgrgriclem  47782  upgrwlkupwlk  47863  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  lincscmcl  48161  lindslinindimp2lem4  48190  lincresunit2  48207  lincresunit3  48210  elfzolborelfzop1  48248  m1modmmod  48255  rege1logbzge0  48293  fllog2  48302  dignn0ldlem  48336  rrx2pnecoorneor  48449  rrx2plord2  48456  rrx2linest  48476  ipolub  48660  ipoglb  48663